Nuprl Lemma : equal_symmetry
13,42
postcript
pdf
T
:Type,
x
,
y
:
T
. (
x
=
y
)
(
y
=
x
)
latex
Up
core
2
,
core
2
Definitions
,
t
T
,
P
Q
,
P
Q
,
P
&
Q
,
P
Q
,
x
:
A
.
B
(
x
)
origin
T:Type, x, y:T. (x = y) 
(y = x) T:Type, x, y:T. (x = y) (y = x) 
T Q Q Qx:A. B(x)